STAMINA

Benchmark
Model:cluster v.1 (CTMC)
Parameter(s)N = 128, T = 2000, t = 20
Property:qos1 (prob-reach-time-bounded)
Invocation (default)
perl ./convert.pl cluster.props label qos1 T 2000
./stamina/stamina/bin/stamina cluster.prism newcluster.props -kappa 1e-9 -const N=128,T=2000,t=20
Execution
Walltime:224.8292214870453s
Return code:0, 0
Relative Error:0.1118767546219302
Log
PRISM
=====

Version: 4.5
Date: Wed Apr 01 10:09:51 UTC 2020
Hostname: cb4ac6bf600d
Memory limits: cudd=1g, java(heap)=2g

Type:        CTMC
Modules:     Left Right Repairman Line ToLeft ToRight 
Variables:   left_n left right_n right r line line_n toleft toleft_n toright toright_n 

Generator:   stamina.InfCTMCModelGenerator
Type:        CTMC

========================================================================
Approximation<1> : kappa = 1.0E-9
========================================================================

---------------------------------------------------------------------

Building model...

Computing reachable states... 9 10017 states
 10017 states
Reachable states exploration and model construction done in 1.456 secs.
Sorting reachable states list...

Time for model construction: 1.581 seconds.

Type:        CTMC
States:      10017 (1 initial)
Transitions: 46759

---------------------------------------------------------------------

Verifying Lower Bound for qos1_min .....

---------------------------------------------------------------------

Model checking: "qos1_min": P=? [ F<=2000 !"minimum" ]

Starting backwards transient probability computation...

Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 111.339 seconds.

Value in the initial state: 0.0011923795603399295

Time for model checking: 111.363 seconds.

Result: 0.0011923795603399295 (value in the initial state)

---------------------------------------------------------------------

Verifying Upper Bound for qos1_max .....

---------------------------------------------------------------------

Model checking: "qos1_max": P=? [ F<=2000 !"minimum" ]

Starting backwards transient probability computation...

Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 111.203 seconds.

Value in the initial state: 0.0011923795603399295

Time for model checking: 111.207 seconds.

Result: 0.0011923795603399295 (value in the initial state)

========================================================================

Property: "qos1": P=? [ F<=2000 !"minimum" ]

ProbMin: 0.0011923795603399295 (value in the initial state)

ProbMax: 0.0011923795603399295 (value in the initial state)

========================================================================